Field of the Invention
The present invention relates to integrated circuit design, and more particularly to electronic design automation tools and tools for verification and analysis of complex designs including memory.
Description of Related Art
Analysis of word-level designs, which leverages design information captured at a higher level than that of individual wires and primitive gates, is a new frontier in hardware verification. At the word level, data path elements and data packets are viewed as entities in their own right as opposed to a group of bit-level signals without any special semantics.
Today's model checking technology works well for checking control oriented properties. Typical model checking consists of an exhaustive state space exploration for verifying that some specified properties hold in the circuit design, and is a very intensive user of computing resources. However, it does not work well with designs where there are wide datapaths, and large memories. Previous approaches tried to speed up the process by reading designer annotations, or computing increasingly precise abstractions of the design. However, annotations are very time consuming for the designer, and the computation of abstractions can be as hard as solving the original problem.
There has been a lot of activity lately around word-level formula decision procedures such as SMT solvers (S. Ranise and C. Tinelli. Satisfiability modulo theories. Trends and Controversies—IEEE Intelligent Systems Magazine, December 2006) and reduction-based procedures like UCLID (R. Bryant, S. Lahiri, and S. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proc. of the Computer Aided Verification Conf., 2002) and BAT (P. Manolios, S. Srinivasan, and D. Vroon. BAT: The bit-level analysis tool. In Proc. of the Computer Aided Verification Conf., 2007). However, as promising as this direction of research is, the use of these procedures for model checking is inherently restricted in that they analyze formulas rather than sequential systems. This has two consequences: First of all, sequential properties can only be checked by these procedures by relying on methods such as induction and interpolation that employ bounded checks to infer unbounded correctness. Second, these procedures do not fit into a transformation-based approach to sequential system verification (J. Baumgartner, T. Gloekler, D. Shanmugam, R. Seigler, G. V. Huben, H. Mony, P. Roessler, and B. Ramanandray. Enabling large-scale pervasive logic verification through multi-algorithmic formal reasoning. In Proc. of the Formal Methods in CAD Conf., 2006), where sequential verification problems are iteratively simplified and processed by any of a large set of back-end model checkers.
Therefore, it would be desirable to efficiently implement for practical word-level model checking of both bounded and unbounded properties for hardware designs. It is further desirable to accomplish this goal with technology that (1) requires little or no additional input from the user, (2) performs well compared to a straight bit-level sequential analysis of a given netlist, and (3) provides the possibility of speedups when there are significant parts of the design that can be treated on the word-level.